the_w:World, e:E, t:.
FairFifo
 (isrcv(kind(e)))
 (match(lnk(kind(e));t;time(e)))
 (onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))|| 
 (- ||snds(lnk(kind(e));t)||)]
 (=
 (msg(a(loc(e);time(e)))
 ( Msg) 

latex

Definitions	t  T, #$n, x:A. B(x), A  B, P & Q, i  j < k, {x:A| B(x)} , , {i..j}, x:AB(x), P  Q, <a, b>, time(e), False, A, {T}, SQType(T), , s ~ t, x:A  B(x), x:A. B(x), World, E, FairFifo, kind(e), isrcv(k), b, lnk(k), match(l;t;t'), m(i;t), onlnk(l;mss), l[i], Msg, , s = t
Lemmas	w-match wf, lnk wf, w-time wf, assert wf, isrcv wf, w-ekind wf, fair-fifo wf, nat wf, w-E wf, world wf, better-w-match-exists, w-match-unique, le wf